(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(assert v0)
(assert (=> v2 v3))
(declare-const v4 Bool)
(assert v3)
(declare-const v7 Bool)
(push)
(push)
(declare-const v10 Bool)
(assert (=> (< (* 0 i4 965) i3) (= v0 (<= (- i4 0 i3 83 (div i4 0)) i3) v3 (= 83 0) (=> v7 (distinct (<= (- i4 0 i3 83 (div i4 0)) i3) (< i2 494) v4 v3 (>= (abs 63) 91) (< i2 494) v1 v2 (= 83 0) (< i2 494) v0)) (= 83 0) v1 (distinct (<= (- i4 0 i3 83 (div i4 0)) i3) (< i2 494) v4 v3 (>= (abs 63) 91) (< i2 494) v1 v2 (= 83 0) (< i2 494) v0))))
(declare-const v12 Bool)
(assert (or (<= (+ (div i4 0) i3 i1) i1) (>= (abs 63) 91) v2 (distinct (<= (- i4 0 i3 83 (div i4 0)) i3) (< i2 494) v4 v3 (>= (abs 63) 91) (< i2 494) v1 v2 (= 83 0) (< i2 494) v0) v12 v10 v10))
(check-sat)
